COMMENT ⊗   VALID 00004 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	NOTES ON  HENSCHEN,OVERBEEK, AND WOS.
 00004 00003	The real problem with the approach is that it is much too simple.
 00006 00004	
 00007 ENDMK
⊗;
NOTES ON  HENSCHEN,OVERBEEK, AND WOS.

It is quite easy to write a language for simple combinatorial applications
of existing rules of inference, such as resolution, factoring and paramodulation.
We have had such for  at least three years directly as an on-line language:

	SET X RE <clauses> <clauses>    for example, will assign X to the
set of resolvents of the two sets of clauses.  This  'programming' of rules of 
inference has also been  available using the TRYTIL feature.

The simple strategies programable by Henschen,Overbeek, and Wos are easy to accomplish
with our program. The hard problems(which I will discuss in a moment) are not
addressed at all in this paper.

Until last October, a clever use of the programmable parts of the prover
required a knowledge of the storage struucture of the clauses, but this
problem has been aleviated  thru the Quam Syntax Directed I-O routines.
As a secondary benefit, since the programs are translated into LISP, we can
compile the resultant rather than be burdened with an interpreter.
The real problem with the approach is that it is much too simple.
True, it is a language for combinatorial manipulations of rules of inference.
As it stands, it is perhaps useful to those knowledgable(or interested)
in the relationships between  various thoerem proving strategies.
If, however you are a user with a problem and wish to state your intuitions
about a problem domain  so that a theorem prover will choose fruitful paths, while
ignoring 'obvously trivial' deductions, something much more grandiose must be
forthcoming.

Can such a language as H O W  be extended to such a task ? True 'the language
is extendable with theoretically no limit'(p.23), but that is not really
relevant.